\chapter{Matematisk formalisme}

Philip J. Davis og Ruben Hers beskriver i \citet{davis1981f} nutidens matematiske formalisme som videnskaben at lave formelle beviser. Den formalistiske matematiker arbejder ud fra et sæt af aksiomer og deduktionsregler og indholdet af matematikken bliver det, der kan udledes deduktivt. Formalisten arbejder ikke med begreber som sandhed, men kun med bevisbarhed. Men Davis og Hearsh skriver også, at det arbejde nutidens matematikere udfører er meget fjernt fra formalistens syn på matematik. 

Idet man laver en fortolkning af aksiomssystemet, kan man snakke om begreberne sandt og falskt. Men disse fortolkninger kommer til at stå udenfor matematikken og det er ikke en formalists opgave at beskæftige sig med dem, fortæller Davis og Hersh. Derfor bliver spørgsmål om eksistens af konsistente fortolkninger og anfægtninger af det valgte aksiomssystem irrelevante.

Beviset er helt centralt i formalistens syn på matematikken og det at lave matematik bliver udelukkende arbejdet med at bevise en hypotese. Bevisets rolle er i høj grad at sikre, at teoremer bliver en logisk konsekvens af aksiomer fri for enhver tvivl. Beviserne mister enhver anden rolle og andre egenskaber end korrekthed svinder væk. Det kan være egenskaber, som f.eks. John W. Dawson, Jr i \citet{Dawson2006a} lægger meget vægt på, som det at være forklarende eller simplelt.

%Desuden bliver mængden af det bevisbare et mål for hvor meget matematik man har lavet. 


%Teoremer bliver en logisk konsekvens af det valgte aksiomssystem, og for formalisten er de fri fra fejl og enhver tvivl. Tilgengæld bliver de uden indhold i den forstand at de ikke udtaler sig om noget. 

%**** OVERVEJ OM ANALYSEN SKAL ADSKILLES KRAFTIGERE OG OM DEN SKAL UDDYBES ****
\chapter{Lakatos' ide om beviser og gendrivelser}
Davis og Hearsh forklarer i \citet{davis1981b} at Lakatos beskæftiger sig med matematik, som den er for matematikere. Det gør, at matematikken bliver en levende størrelse, der konstant vokser i en iterativ proces af debat, strid og tvivl udmundende i teorier med øget pålidelighed. 

I denne kontekst forstår han ikke beviser som den mekaniske proces, der sikrer korrekthed af et resultat, men istedet som "\dots explanations, justifications, elaborations which make the conjecture more plausible, more convincing, while it is being made more detailed and accurate under the pressure of counterexamples", \cite[Side 347]{davis1981b}. Denne ide og dens konsekvenser analyserer Henrik Kragh Sørensen i \cite[Afsnit 6.2]{HKS2005a}.

I citatet er antydet en dialektik mellem beviser og modeksempler og denne proces uddyber Kragh i 4 trin. Man går fra en primitiv formodning over udarbejdelsen af et bevis til at lede efter modeksempler på formodningen for at ende i en analyse af hele beviset. I udarbejdelsen af beviset opdeles det typisk i en række lemmaer og dermed kan modeksempler både være lokale møntet på enkelte lemmaer eller globale på selve formodningen. Det er en proces, der ofte gennemgåes flere gange og på den måde får beviser en foranderlig og midlertidig karakter, men opnår også en meget central plads i den matematiske metode. 

Kragh nævner også, at beviserne, i denne rolle, er med til at skabe nye begreber. Det kan ske både for at opnå gyldighed for centrale beviser, men også i forbindelse med bestræbelser på at formulere eller bevise generaliseringer af sætninger. Til slut nævner Kragh, at man kan risikere at prisen for at stræbe efter præcision eller formalisering bliver indholdet.  


%Dette uddyber Kragh i \citet{HKS2005a} hvor han beskriver processen at lave matematik opdelt i 4 trin: Den indledende formulering af en primitive formodning, udarbejdelsen af et bevis der opløser formodningen i lemmaer, jagten på lokale eller globale modeksempler og til sidst en analyse af hele beviset. Derudover skriver han at det kan være nødvendigt at løbe processen igennem flere gange. 
% PROCESSEN ER VEL LIGEGYLDIG IFT BEVISERS ROLLE?

\chapter{Om at genbevise sætninger}

I \citet{Dawson2006a} gennemgår John W. Dawson, Jr. hans syn på beviser som indledning til en række forskellige grunde til at genbevise sætninger. Hans definition af et bevis er en række argumenter hvorom det samtidige matematik samfund har konsensus dets gyldighed. Årsagerne (3.1), (3.5) og (3.8) fra \citet{Dawson2006a} vil medtages i analysen:

\begin{enumerate}
\item For at fjerne huller eller utilstrækkeligheder i tidligere argumenter. \label{pkt:1}
\item For at udvide eller generalisere den til andre områder. \label{pkt:2}
\item For at øge pålideligheden. \label{pkt:3}
\end{enumerate}

Dawson skriver at oftest er det i tilfælde af resultater man accepterer som korrekte, så man skal forstå huller og utilstrækkeligheder, i punkt \ref{pkt:1}, som argumenter, der ikke tilfredsstiller matematikernes stræben efter klarhed. Han siger her også flere steder, at beviser ikke i alle tilfælde kan tilfredsstille alle grunde på en gang, da der kan findes modstridende argumenter. Det nævner han både for punkt \ref{pkt:1} og \ref{pkt:2}, hvor man i det første kan foretrække indviklede konstruktivistiske argumenter og i det andet kan en udvidelse af en sætning kræve indførelsen af mere avanceret matematik. 

Når et genbevis kan øge pålideligheden for sætningen understreger han at et bevis ikke er endegyldigt korrekt. Tilgengæld beskriver han matematikkens pålidelighed som et kabel, hvor hver enkelt fiber er med til at give styrke og konkluderer "Most mathematical results can be reached in so many ways, that their incorrectness is simply unthinkable". \cite[Side 281 midt]{Dawson2006a}

For en formalist vil både punkt 1 og 3 være irrelevante. Da man har et formelt bevis, har man det højest mulige niveau af pålidelighed og der kan ikke være huller eller utilstrækkeligheder. Selvom Dawson ikke mener man kan anvende hans idéer om genbevisning på formelle beviser kan man godt sige at punkt 2 er relevant. Problemet er her, at formalismen ikke beskæftiger sig med hvordan man finder den udvidede hypotese, så matematikken starter, i formalistens syn, først idét man har fundet den udvidede eller generaliserede formodning. 

Davis og Hersh kommer ikke ind på muligheden for at udvide eller generalisere sætninger og det passer dårligt på den dialektiske proces der skal gøre formodningen mere detaljeret og præcis. 

De behandler ikke det, at genbevise direkte, men man kan overføre Lakatos' ideer på argumenterne for at genbevise resultater. Da et bevis i Lakatos' forstand er flydende vil det være meget relevant at søge andre beviser i arbejdet med at gøre en formodning mere sikker. Dermed bliver punkt 1 og 3 meget væsentlige både i den itererende Lakatoske dialektik, men andre beviser for det samme vil for Lakatosianere også være med til at overbevise dem. 

